The present invention relates to the field of computer-aided design of integrated circuits and, in particular, to testing the equivalence of digital logic circuits.
Recent increases in the complexity of modern integrated circuits (ICs) have made it imperative to verify design correctness prior to fabrication. The verification of design correctness, prior to fabrication, is essential because any design flaw detected after fabrication can have a severe economic impact in terms of increased time-to-market and reduced profit margins.
One of the main steps undertaken in verifying design correctness is that of equivalence checking between two logic circuit designs that belong to different development stages of designing the IC. Equivalence checking is performed using equivalence checkers, which are usually implemented in software. The equivalence checkers build mathematical models of the two logic circuit designs, and mathematically verify that the logics implemented by the two designs are the same. If an equivalence checker determines that the two circuit designs output the same values for a given input at a given point of time, then the two circuits are termed as equivalent to one another. Further, the circuits being tested for equivalence can be classified into two categories: combinational circuits and sequential circuits. A combinational circuit is a circuit whose output depends entirely on the values of the inputs to the circuit. A simple example of a combinational circuit is a series of interconnected AND gates, in which none of the outputs is fed back to the AND gates. A sequential circuit is a circuit whose output depends, in addition to input values, on the previous values of the sequential elements of the circuit. Therefore, a sequential circuit comprises one or more combinational circuits wherein the output values may be fed back to the combinational circuits via storage elements. The storage elements may be implemented by using flip flops, latches or registers.
There are many equivalence checking techniques and tools for equivalence checking in combinational circuits. The research paper titled ‘Equivalence Checking Using Cuts and Heaps’, by Andreas Kuehlmann and Florian Krohm, Proceedings of the 34th annual ACM IEEE conference on Design automation, pages: 263-268, describes one such approach. Another technique is described in research paper titled ‘Combinational Equivalence Checking through Function Transformation’, by Hee Hwan Kwak, InHo Moon, James H. Kukula and Thomas R. Shiple, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, pages: 526-533. Examples of software tools used for combinational equivalence checking are Conformal LEC from Cadence Design Systems; Formality® from Synopsys, Inc; and FormalPro from Mentor Graphics.
Equivalence checking in the case of sequential circuits is relatively complex. This is because of the presence of storage elements, which are responsible for generating different sets of output values for the same set of input values. Two steps are performed to check the equivalence between two sequential circuits. In the first step, a mapping between the corresponding storage elements of the two circuits is performed. This step is also known as latch mapping or register mapping. Once the corresponding storage elements are identified, it is possible to decompose the circuits into various combinational blocks. Therefore, in the second step, the equivalence is determined by checking if the corresponding combinational blocks are equivalent.
There are many techniques in the art for performing the mapping of storage elements. One such technique has been described in U.S. Pat. No. 6,496,955, titled ‘Latch Mapper’ assigned to Sun Microsystems, Inc., Santa Clara, Calif. Another technique is mentioned in U.S. Pat. No. 6,247,163, titled ‘Method and System of Latch Mapping for Combinational Equivalence Checking’, assigned to Cadence Design Systems, Inc., San Jose, Calif. However, these techniques are not failsafe and may fail in complex sequential circuits, which involve a large number of storage (or memory) elements. Further, in some commercially available tools, there is the requirement of one-to-one latch mapping between the two circuits being compared. In these tools, the correspondence between the storage elements must be provided by the user of the tool.
In light of the above discussion, there is a need for a method that makes the task of equivalence checking in sequential circuits simpler and more effective. A need also exists for a method that reduces or minimizes the number of storage elements in a sequential circuit, so that equivalence checking is made easier.